es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id }Prop).
e<e'.P(e)  first(e') & P(pred(e'))  e<pred(e').P(e) 

latex

Definitions	A & B, x:A. B(x), e<e'.P(e), t  T, P  Q, x:A. B(x), b, False, A, loc(e), Id, pred(e), 1of(t), E, x(s), P  Q, ES, Prop, x. t(x), first(e), P  Q, P & Q, P  Q, (e <loc e'), True, T, {T}
Lemmas	es-pred-locl, es-locl wf, squash wf, true wf, es-locl-iff, not wf, assert wf, es-first wf, existse-before wf, es-E wf, event system wf, es-pred wf, Id wf, es-loc wf, es-loc-pred